x:Id, L:Knd List. only members of L read x  MsgA 

latex

Definitions	t  T, Id, Knd, type List, x.A(x), x:A. B(x), x. t(x), x : v, IdLnk, , x:AB(x), Void, Type, Top, x:AB(x), State(ds), Prop, mk-ma, only members of L read x, MsgA
Lemmas	mk-ma wf, ma-state wf, top wf, fpf-empty wf, IdLnk wf, fpf-single wf, Knd wf, Id wf